Vive la Diff\'erence: Paxos vs. Viewstamped Replication vs. Zab

摘要

Paxos, Viewstamped Replication, and Zab are replication protocols that ensurehigh-availability in asynchronous environments with crash failures. Variousclaims have been made about similarities and differences between theseprotocols. But how does one determine whether two protocols are the same, andif not, how significant the differences are? We propose to address these questions using refinement mappings, whereprotocols are expressed as succinct specifications that are progressivelyrefined to executable implementations. Doing so enables a principledunderstanding of the correctness of the different design decisions that wentinto implementing the various protocols. Additionally, it allowed us toidentify key differences that have a significant impact on performance.